3.2.1.2 Assertions

3.2.1.2 Assertions

RTS module supports all assertions in CSP Module. There are some notes below that users should be awared.

Note: Based on the clock zone abstraction, RTS module can handle dense time systems (in contrast to discrete time or continuous time), i.e., all clock values can be rational numbers. RTS module supports only integer numbers, since a set of rational numbers can be converted to an "equivalent" set of integer number by multiplying the lowest common multiple.

Linear Temporal Logic (LTL)

In RTS module, we support the full set of LTL syntax except the X (next)operator.

Refinement/ Equivalence

In RTS module, the refinement and equivalence checking consider only events now. The time transitions are ignored.